(module equal-types (lib "eopl.ss" "eopl")
  
  (provide equal-types?)
  
  (define equal-types?
    (lambda (ty1 ty2)
      (equal-up-to-gensyms? ty1 ty2)))
  
  ;; sexp = symbol | (list-of sexp)
  ;; alist = (list (pair tvar-sym tvar-sym))
  ;; a tvar-sym is a symbol ending with a digit.
  
  ;; equal-up-to-gensyms? : sexp * sexp -> bool
  
  (define equal-up-to-gensyms?
    (lambda (sexp1 sexp2)
      (equal?
       (apply-subst-to-sexp (canonical-subst sexp1) sexp1)
       (apply-subst-to-sexp (canonical-subst sexp2) sexp2))))
  
  ;; canonicalize : sexp -> alist
  ;; replaces all tvar-syms with tvar1, tvar2, etc.
  (define canonical-subst
    (lambda (sexp)
      ;; loop : sexp * alist -> alist
      (let loop ((sexp sexp) (table '()))
        (cond
          ((null? sexp) table)
          ((tvar-sym? sexp) 
           (cond
             ((assq sexp table) ; sexp is already bound, no more to
              ; do 
              table)
             (else 
              (cons 
               ;; the length of the table serves as a counter!
               (cons sexp (ctr->tvar (length table))) 
               table))))
          ((pair? sexp)
           (loop (cdr sexp)
                 (loop (car sexp) table)))
          (else table)))))
  
  (define tvar-sym?
    (lambda (sym)
      (and (symbol? sym)
           (char-numeric? (car (reverse (symbol->list sym)))))))
  
  (define symbol->list
    (lambda (x) (string->list (symbol->string x))))
  
  (define apply-subst-to-sexp
    (lambda (subst sexp)
      (cond
        ((null? sexp) sexp)
        ((tvar-sym? sexp)
         (cdr (assq sexp subst)))
        ((pair? sexp)
         (cons
          (apply-subst-to-sexp subst (car sexp))
          (apply-subst-to-sexp subst (cdr sexp))))
        (else sexp))))
  
  (define ctr->tvar
    (lambda (n)
      (string->symbol
       (string-append
        "tvar"
        (number->string n)))))
  )